es:ES, e1:E, e2:{e:E| loc(e) = loc(e1)  Id} . e(e1,e2].False  e2 loc e1  

latex

Definitions	x:A. B(x), P  Q, e(e1,e2].P(e), P  Q, P & Q, P  Q, t  T, , False
Lemmas	es-E wf, es-locl wf, es-le wf, false wf, es-locl transitivity2, es-locl irreflexivity, Id wf, es-loc wf, event system wf